Section: New Results

Security by Typing for Cryptographic Protocol Implementations

Participants : Karthikeyan Bhargavan [correspondant] , Cédric Fournet [MSR Cambridge] , Andrew D. Gordon [MSR Cambridge] , Alfredo Pironti.

We propose to use refinement typing to verify the security of cryptographic protocol implementations. Our method is based on declaring and enforcing invariants on the usage of cryptography. We develop cryptographic libraries that embed a logic model of their cryptographic structures and that specify preconditions and postconditions on their functions so as to maintain their invariants.

We implement the method for protocols coded in F# and verified using F7, our SMT-based typechecker for refinement types, that is, types carrying formulas to record invariants. As illustrated by a series of programming examples, our method can flexibly deal with a range of different cryptographic constructions and protocols [24] .

We are currently evaluating this method on a fully-fledged implementation of TLS. While previous uses of typing for cryptographic protocol implementations focused on the symbolic model of cryptography, we use a new technique by Fournet et al to develop computational proofs for our implementations. Our TLS implementation consists of 6000 lines of code. We have currently annotated and verified about half of this implentation.

We recently published a tutorial on our verification method as part of the proceedings of FOSAD 2010, and a journal paper on our type system at TOPLAS [20] .